poss:(ES{i}{i'}), T:Type{i}, s:T, i:Id, P:(possible-event{i:l}(poss){i'}),
R:(possible-event{i:l}(poss)possible-event{i:l}(poss){i'}), Rs:(TT{i'}).
EquivRel(possible-event{i:l}
EquivRel(possible-event(poss);_1,_2.R(_1,_2))
 (e, e':possible-event{i:l}(poss).
 poss-consistent(i;T;s;e;Rs)  poss-consistent(i;T;s;e';Rs)  (R(e,e')))
 (ma-knows{i:l}
 (ma-knows(poss; i; T; s; P; Rs; R))
 ma-knows{i:l}
 ma-knows(poss; i; T; s; (e.es-knows{i:l}(poss; R; P; e)); Rs; R) 

latex

Definitions	f(a), x:A. B(x), t  T, P  Q, Trans(T;x,y.E(x;y)), x:A  B(x), P & Q, EquivRel(T;x,y.E(x;y)), PossibleEvent(poss), K(P)@e, poss-consistent(i;T;s;ev;R), False, A, x:AB(x), Type, Atom$n, Id, A c B, Void, , ES, x,y. t(x;y), Ki(P)@s
Lemmas	not wf, equiv rel wf, Id wf, event system wf, es-knows-not, es-knows wf, poss-consistent wf, possible-event wf